Recursion breaks termination:

Recursion + Fixed Points

In STLC we want to preserve termination, so we’ll instead create a new language for recursion: PCF. Which is (some version of) STLC + Fixed Points.

STLC vs PCF

PCF has no strings, and has partial functions instead of total functions. We also do pure natural numbers as successors of zero. We also have a function for testing for zero.

Partial Functions

A partial function is a function that may not be defined for all inputs.